Nuprl Lemma : add_mono_wrt_le_rw
12,41
postcript
pdf
a
,
b
,
n
:
. {(
a
b
)
((
a
+
n
)
(
b
+
n
))}
latex
ProofTree
Definitions
{
T
}
Lemmas
add
mono
wrt
le
origin
a, b, n:
. {(a 
b) 
((a+n) (b+n))}
a, b, n:. {(a b) ((a+n) (b+n))}